import nltk.inference
import unittest
import sys

class TestParallelProverBuilderCommand(unittest.TestCase):
    """
        Test the nltk.ParallelProverBuilderCommand class which runs Mace4 and Prover9 in parallel.
        The first one that finishes determines the result:
        api.py (ParallelProverBuilderCommand): 'Because the theorem prover result is the opposite of the model builder
        result, we will treat self._result as meaning "proof found/no model found".'
        
        There is an error on line 520 in nltk\inference\api.py
        tp_thread = TheoremToolThread(lambda: BaseProverCommand._prove(self, verbose), tp_result, verbose, 'TP')
        should be:
        tp_thread = TheoremToolThread(lambda: BaseProverCommand.prove(self, verbose), tp_result, verbose, 'TP')
    """

    def setUp(self):
        prover9 = nltk.Prover9()
        #prover9 = nltk.ResolutionProver()
        #prover9 = nltk.TableauProver
        mace = nltk.Mace()
        self.prover = nltk.ParallelProverBuilderCommand(prover9, mace)

#    def testProver9(self):
#        rules = ['mortal(socrates)', '-mortal(socrates)']
#        new_assumptions = []
#        lp = nltk.LogicParser()
#        for rule in rules:
#            new_assumptions.append(lp.parse(rule))
#        #prover9 = nltk.Prover9()
#        #print prover9._prove(assumptions=new_assumptions, verbose=True)[0]

    def testSatisfiable01(self):
        rules = ['mortal(Socrates)'
                 , 'mortal(Berta)'
                 , 'mortal(Menno)'
                 , 'man(Socrates)'
                 , 'man(Menno)'
                 , 'cow(Berta)'
                 , 'Menno != Socrates'
                 , 'all x. (cow(x) -> -man(x))'
                 ]
        #goal = 'some p. (mortal(p) & -man(p))'  # True
        #goal = 'some p. (mortal(p) & man(p))' # Somebody is mortal and a man # True
        #goal = 'some p. -mortal(p)' # False
        goal = 'all p. (mortal(p) -> man(p))' # False
        rule_expressions = []
        goal_expression = None
        lp = nltk.LogicParser()
        for rule in rules:
            rule_expressions.append(lp.parse(rule))
        goal_expression = lp.parse(goal)
        self.prover.add_assumptions(rule_expressions)
        self.prover._goal = goal_expression
        proofFound = self.prover.prove(verbose=False)
        print "Proof found/no model found: " + str(proofFound)
        print 60*'='
        self.assertFalse(proofFound)
        if proofFound: # no model found
            pass
            #print self.prover.proof()
            #self.prover.get_prover()
        else:
            pass
            # counter model found
            #print self.prover.model()

    def testSatisfiable02(self):
        rules = ['mortal(Socrates)'
                 , 'mortal(Menno)'
                 , 'man(Socrates)'
                 , 'man(Menno)'
                 , 'Menno != Socrates'
                 ]
        #goal = 'some p. (mortal(p) & -man(p))'  # True
        #goal = 'some p. (mortal(p) & man(p))' # Somebody is mortal and a man # True
        #goal = 'some p. -mortal(p)' # False
        goal = 'all p. (mortal(p) -> man(p))' # False
        rule_expressions = []
        goal_expression = None
        lp = nltk.LogicParser()
        for rule in rules:
            rule_expressions.append(lp.parse(rule))
        goal_expression = lp.parse(goal)
        self.prover.add_assumptions(rule_expressions)
        self.prover._goal = goal_expression
        proofFound = self.prover.prove(verbose=False)
        print "Proof found/no model found: " + str(proofFound)
        print 60*'='
        self.assertFalse(proofFound)
        if proofFound: # no model found
            pass
            #print self.prover.proof()
            #self.prover.get_prover()
        else:
            pass
            # counter model found
            #print self.prover.model()

    def testSatisfiable03(self):
        rules = ['mortal(Socrates)'
                 , 'mortal(Menno)'
                 , 'man(Socrates)'
                 , 'cow(Menno)'
                 , 'Menno != Socrates'
                 , 'all x. (cow(x) -> -man(x))'
                 ]
        #goal = 'some p. (mortal(p) & -man(p))'  # True
        #goal = 'some p. (mortal(p) & man(p))' # Somebody is mortal and a man # True
        #goal = 'some p. -mortal(p)' # False
        goal = '-mortal(Socrates)' # False
        rule_expressions = []
        goal_expression = None
        lp = nltk.LogicParser()
        for rule in rules:
            rule_expressions.append(lp.parse(rule))
        
        goal_expression = lp.parse(goal)
        self.prover.add_assumptions(rule_expressions)
        self.prover._goal = goal_expression
        proofFound = self.prover.prove(verbose=False)
        print "testSatisfiable03: Proof found/no model found: " + str(proofFound)
        print 60*'='
        self.assertFalse(proofFound)
        if proofFound: # no model found
            pass
            #print self.prover.proof()
            #self.prover.get_prover()
        else:
            pass
            # counter model found
            #print self.prover.model()
        #print self.prover.proof()
           
    def testSatisfiable04(self):
        rules = ['mortal(Socrates)'
                 , 'mortal(Menno)'
                 , 'man(Socrates)'
                 , 'cow(Menno)'
                 , 'Menno != Socrates'
                 , 'all x. (cow(x) -> -man(x))'
                 ]
        #goal = 'some p. (mortal(p) & -man(p))'  # True
        #goal = 'some p. (mortal(p) & man(p))' # Somebody is mortal and a man # True
        #goal = 'some p. -mortal(p)' # False
        goal = 'cow(Menno)' # True statement
        rule_expressions = []
        goal_expression = None
        lp = nltk.LogicParser()
        for rule in rules:
            rule_expressions.append(lp.parse(rule))
        
        goal_expression = lp.parse(goal)
        self.prover.add_assumptions(rule_expressions)
        self.prover._goal = goal_expression
        proofFound = self.prover.prove(verbose=False)
        print "testSatisfiable04: Proof found/no model found: " + str(proofFound)
        print 60*'='
        self.assertTrue(proofFound)
        if proofFound: # no model found
            pass
            #print self.prover.proof()
            #self.prover.get_prover()
        else:
            pass
            # counter model found
            #print self.prover.model()
        #print self.prover.proof()           
            
    def testSatisfiable05(self):
        rules = ['mortal(Socrates)'
                 , 'mortal(Menno)'
                 , 'man(Socrates)'
                 , 'cow(Menno)'
                 , 'Menno != Socrates'
                 , 'all x. (cow(x) -> -man(x))'
                 ]
        #goal = 'some p. (mortal(p) & -man(p))'  # True
        #goal = 'some p. (mortal(p) & man(p))' # Somebody is mortal and a man # True
        #goal = 'some p. -mortal(p)' # False
        goal = '-man(Menno)' # True statement
        rule_expressions = []
        goal_expression = None
        lp = nltk.LogicParser()
        for rule in rules:
            rule_expressions.append(lp.parse(rule))
        
        goal_expression = lp.parse(goal)
        self.prover.add_assumptions(rule_expressions)
        self.prover._goal = goal_expression
        proofFound = self.prover.prove(verbose=False)
        print "testSatisfiable05: Proof found/no model found: " + str(proofFound)
        print 60*'='
        self.assertTrue(proofFound)
        if proofFound: # no model found
            pass
            #print self.prover.proof()
            #self.prover.get_prover()
        else:
            pass
            # counter model found
            #print self.prover.model()
        #print self.prover.proof()
        
    def testSatisfiable06(self):
        rules = ['mortal(Socrates)'
                 , 'mortal(Menno)'
                 , 'man(Socrates)'
                 , 'cow(Menno)'
                 , 'Menno != Socrates'
                 , 'all x. (cow(x) -> -man(x))'
                 ]
        #goal = 'some p. (mortal(p) & -man(p))'  # True
        #goal = 'some p. (mortal(p) & man(p))' # Somebody is mortal and a man # True
        #goal = 'some p. -mortal(p)' # False
        goal = 'man(Menno)' # False statement
        rule_expressions = []
        goal_expression = None
        lp = nltk.LogicParser()
        for rule in rules:
            rule_expressions.append(lp.parse(rule))
        
        goal_expression = lp.parse(goal)
        self.prover.add_assumptions(rule_expressions)
        self.prover._goal = goal_expression
        proofFound = self.prover.prove(verbose=False)
        print "testSatisfiable06: Proof found/no model found: " + str(proofFound)
        print 60*'='
        self.assertFalse(proofFound)
        if proofFound: # no model found
            pass
            #print self.prover.proof()
            #self.prover.get_prover()
        else:
            pass
            # counter model found
            #print self.prover.model()
        #print self.prover.proof()          
                    
    def testUnsatisfiable(self):
        rules = ['mortal(Socrates)', '-mortal(Socrates)']
        new_assumptions = []
        lp = nltk.LogicParser()
        for rule in rules:
            new_assumptions.append(lp.parse(rule))
        self.prover.add_assumptions(new_assumptions)
        proofFound = self.prover.prove(verbose=False)
        print "testUnsatisfiable: Proof found/no model found: " + str(proofFound)
        print 60*'='
        self.assertTrue(proofFound)  
        if proofFound: # no counter model found
            pass
            #print self.prover.proof()
            #self.prover.get_prover()
        else:
            pass
            # counter model found
            #print self.prover.model()        
        #print self.prover.proof(True)

    def testEventSemanticsProof01(self):
        rules = [
                 'exists e.(bark(e) & agent(e,John))' # John barks
                 , 'exists e.dog(John)'
                 ]
        goal = '-exists e.dog(John)' # False
        proofExpected = False
        proofFound = self.proofTester(rules, goal)
        self.assertEqual(proofFound, proofExpected)
        print 60*'='        
        this_function_name = sys._getframe().f_code.co_name
        print this_function_name + ": Proof found/no model found: " + str(proofFound)
        
    def testEventSemanticsProof02(self):
        rules = [
                 'exists e.(bark(e) & agent(e,John))' # John barks
                 , 'exists e.dog(John)'
                 ]
        goal = 'exists e.dog(John)' # True statement
        proofExpected = True
        proofFound = self.proofTester(rules, goal)   
        self.assertEqual(proofFound, proofExpected)
        print 60*'='        
        this_function_name = sys._getframe().f_code.co_name
        print this_function_name + ": Proof found/no model found: " + str(proofFound)
        
        
    def testEventSemanticsProof03(self):
        rules = [
                 'exists e.(bark(e) & agent(e,John))' # John barks
                 , 'exists e.dog(John)'
                 ]
        goal = 'dog(John)' # True
        proofExpected = True
        proofFound = self.proofTester(rules, goal)
        self.assertEqual(proofFound, proofExpected)
        print 60*'='        
        this_function_name = sys._getframe().f_code.co_name
        print this_function_name + ": Proof found/no model found: " + str(proofFound)

    def testEventSemanticsProof04(self):
        rules = [
                 'exists e.(bark(e) & agent(e,John))' # John barks
                 , 'exists e.dog(John)'
                 ]
        goal = '-dog(John)' # False
        proofExpected = False
        proofFound = self.proofTester(rules, goal)
        self.assertEqual(proofFound, proofExpected)
        print 60*'='        
        this_function_name = sys._getframe().f_code.co_name
        print this_function_name + ": Proof found/no model found: " + str(proofFound)        

    def testEventSemanticsProof05(self):
        rules = [
                 'exists e.(bark(e) & agent(e,John))' # John barks
                 , 'exists e.dog(John)'
                 ]
        goal = 'agent(John)' # unknown
        proofExpected = False
        proofFound = self.proofTester(rules, goal)
        self.assertEqual(proofFound, proofExpected) # will fail sometimes
        print 60*'='
        this_function_name = sys._getframe().f_code.co_name
        print this_function_name + ": Proof found/no model found: " + str(proofFound)

    def testEventSemanticsProof06(self):
        rules = [
                 'exists e.(bark(e) & agent(e,John))' # John barks
                 , 'exists e.dog(John)'
                 ]
        goal = 'exists e.agent(e, John)' # True
        proofExpected = True
        proofFound = self.proofTester(rules, goal)
        self.assertEqual(proofFound, proofExpected)
        print 60*'='
        this_function_name = sys._getframe().f_code.co_name
        print this_function_name + ": Proof found/no model found: " + str(proofFound)
        
    def testEventSemanticsProof07(self):
        rules = [
                 'exists e.(bark(e) & agent(e,John))' # John barks
                 , 'exists e.dog(John)'
                 ]
        goal = 'exists e.(bark(e) & agent(e,John))' # True
        proofExpected = True
        proofFound = self.proofTester(rules, goal)
        self.assertEqual(proofFound, proofExpected)
        print 60*'='
        this_function_name = sys._getframe().f_code.co_name
        print this_function_name + ": Proof found/no model found: " + str(proofFound)        

    def testEventSemanticsProof08(self):
        rules = [
                 'exists e.(bark(e) & agent(e,John))' # John barks
                 , 'exists e.dog(John)'
                 ]
        goal = 'exists e.(hates(e) & agent(e,John))' # False
        proofExpected = False
        proofFound = self.proofTester(rules, goal)
        self.assertEqual(proofFound, proofExpected)
        print 60*'='
        this_function_name = sys._getframe().f_code.co_name
        print this_function_name + ": Proof found/no model found: " + str(proofFound)    

    def testEventSemanticsProof09(self):
        rules = [
                 'exists e.(bark(e) & agent(e,John))' # John barks
                 , 'exists e.(in(e,Amsterdam))'
                 ]
        goal = 'exists e.(in(e,Rotterdam))' # False
        proofExpected = False
        proofFound = self.proofTester(rules, goal)
        self.assertEqual(proofFound, proofExpected)
        print 60*'='
        this_function_name = sys._getframe().f_code.co_name
        print this_function_name + ": Proof found/no model found: " + str(proofFound)  
         
    def testEventSemanticsProof10(self):
        rules = [
                 'exists e.(bark(e) & agent(e,John))' # John barks
                 , 'exists e.(in(e,Amsterdam))'
                 ]
        goal = 'exists e.(in(e,Amsterdam))' # True
        proofExpected = True
        proofFound = self.proofTester(rules, goal)
        self.assertEqual(proofFound, proofExpected)
        print 60*'='
        this_function_name = sys._getframe().f_code.co_name
        print this_function_name + ": Proof found/no model found: " + str(proofFound)  

    def testEventSemanticsProof11(self):
        rules = [
                 'exists e.(bark(e) & agent(e,John))' # John barks
                 , 'exists e.(in(e,Amsterdam))'
                 ]
        goal = 'exists e.(in(e,Amsterdam) & bark(e))' # False, the 'e' in the rules are not bound, thus not the same
        proofExpected = False
        proofFound = self.proofTester(rules, goal)
        self.assertEqual(proofFound, proofExpected)
        print 60*'='
        this_function_name = sys._getframe().f_code.co_name
        print this_function_name + ": Proof found/no model found: " + str(proofFound) 

    def testEventSemanticsProof12a(self):
        rules = [
                 r'\e2.(exists e2.(in(e2,Amsterdam) & bark(e2)))'
                 ]
        goal = 'exists e.(in(e,Amsterdam) & bark(e))' # True
        proofExpected = True
        proofFound = self.proofTester(rules, goal)
        self.assertEqual(proofFound, proofExpected) #fails sometimes.. What should the real result be?
        print 60*'='
        this_function_name = sys._getframe().f_code.co_name
        print this_function_name + ": Proof found/no model found: " + str(proofFound)
        
    def testEventSemanticsProof12b(self):
        rules = [
                 r'exists e2.(in(e2,Amsterdam) & bark(e2))'
                 ]
        goal = 'exists e.(in(e,Amsterdam) & bark(e))' # True
        proofExpected = True
        proofFound = self.proofTester(rules, goal)
        self.assertEqual(proofFound, proofExpected)
        print 60*'='
        this_function_name = sys._getframe().f_code.co_name
        print this_function_name + ": Proof found/no model found: " + str(proofFound)
        
    def testEventSemanticsProof12c(self):
        rules = [
                 r'\e33.(  (\e2.(exists e2.(in(e2,Amsterdam))) (e33))  &  (\e1.(exists e1.(bark(e1))) (e33))  ) (e9)'
                 ]
        goal = 'exists e8.(in(e8,Amsterdam) & bark(e8))' # True
        proofExpected = False
        proofFound = self.proofTester(rules, goal)
        self.assertEqual(proofFound, proofExpected)
        print 60*'='
        this_function_name = sys._getframe().f_code.co_name
        print this_function_name + ": Proof found/no model found: " + str(proofFound)
        
    def testEventSemanticsProof13(self):
        rules = [
                 '\e33.(  (exists e2.(in(e2,Amsterdam))) & (exists e2.(bark(e2)))  ) (e)',
                 'exists e1.(bark(e1))'
                 ]
        goal = 'exists e.(in(e,Amsterdam) & bark(e))' # True
        proofExpected = True
        proofFound = self.proofTester(rules, goal)
        self.assertEqual(proofFound, proofExpected)
        print 60*'='
        this_function_name = sys._getframe().f_code.co_name
        print this_function_name + ": Proof found/no model found: " + str(proofFound)                  
                                                       
    def proofTester(self, rules, goal, verbose=False):
        """
            @param rules: list of expression in string format
            @param goal: the goal expression that will be used in the prover
        """
        rule_expressions = []
        goal_expression = None
        lp = nltk.LogicParser()
        for rule in rules:
            rule_expressions.append(lp.parse(rule))
        
        goal_expression = lp.parse(goal)
        self.prover.add_assumptions(rule_expressions)
        self.prover._goal = goal_expression
        proofFound = self.prover.prove(verbose=verbose)
        if proofFound: # no model found
            pass
            #print self.prover.proof()
            #self.prover.get_prover()
        else:
            pass
            # counter model found
            #print self.prover.model()
        #print self.prover.proof() 
        return proofFound     
        
if __name__ == "__main__":
    unittest.main()

